(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : _14 (b = b) ?1 : _23 (c = c) ?2 : _32 (a′ = a′) (b = b) (b′ = b′) ?3 : _45 (a′ = a′) (b′ = b′) (c = c) (c′ = c′) Sort _14 [ at Issue3340.agda:16,19-23 ] Sort _23 [ at Issue3340.agda:17,19-23 ] Sort _32 [ at Issue3340.agda:21,33-37 ] Sort _45 [ at Issue3340.agda:22,44-48 ] " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3)))
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: _14 (b = b) ———————————————————————————————————————————————————————————— b : B a a : A" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: _23 (c = c) ———————————————————————————————————————————————————————————— c : C b b : B b.a b.a : A" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: _32 (a′ = a′) (b = b) (b′ = b′) ———————————————————————————————————————————————————————————— b′ : B a′ b : B a a : A a′ : A" nil)
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: _45 (a′ = a′) (b′ = b′) (c = c) (c′ = c′) ———————————————————————————————————————————————————————————— c′ : C b′ c : C b b′ : B a b : B b.a b.a : A a : A a′ : A" nil)
